Lagrange interpolation

\begin{theorem} Given distinct real numbers $x_1, \ldots, x_{n+1}$ and any real numbers $y_1, \ldots, y_{n+1}$, there exists a unique polynomial $P$ of degree $\le n$ such that $P(x_i) = y_i$ for all $i$. \end{theorem}

import Mathlib

open Real Polynomial

example {n : ℕ} (x : Fin (n + 1) → ℝ)
    (hx : ∀ i j, x i = x j → i = j) (y : Fin (n + 1) → ℝ) :
    ∃! P : Polynomial ℝ, P.degree ≤ n ∧ ∀ i, P.eval (x i) = y i := by sorry